A:Type, eq:EqDecider(A), f:a:A fp Top, L:(A List).
l_disjoint(A;f.1;L)  (a:A. (a  dom(f))  ((a  L))) 

latex

Definitions	a:A fp B(a), l_disjoint(T;l1;l2), x  dom(f), P  Q, P  Q, False, P & Q, P  Q, , b, deq-member(eq;x;L), t.1, x. t(x), A, (x  l), Top, EqDecider(T), x:A. B(x), t  T
Lemmas	assert-deq-member, deq wf, top wf, l member wf, not wf, pi1 wf, deq-member wf, assert wf